FDL - Nuprl Lemma : assert-eq-lnk

Nuprl Lemma : assert-eq-lnk

a,b:IdLnk. (

eq_lnk(a; b))

(a = b)

Definitions x:A. B(x), P Q, eq_lnk(a; b), P Q, prop{i:l}, P Q, t T, P Q

Lemmas iff functionality wrt iff, assert wf, eqof wf, idlnk-deq wf, deq property, IdLnk wf